Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, wir beenden nun zunächst mal das Thema mehrsortige Datentypen mit einer längeren

Anleitung zum Thema mehrsortige Induktion und gehen dann im zweiten Teil der Sitzung

zum Dualen über, das heißt wir gehen über von Daten zu Codaten, Sie dürfen also gespannt sein.

Wir erinnern uns noch mal an, wir erinnern uns an unseren zweisortigen Datentyp von

beliebig verzweigenden Bäumen. Da werden also zwei Datentypen gleichzeitig definiert

mit TreeR und ForestR, mit vier Konstruktoren. Der erste war dieser Blattkonstruktor, der ein

Element unseres Parameter-Datentyps a für die Einträge nimmt und den in ein Blatt umwandelt.

Das nächste dann dieser Konstruktor Node, der einen Wald nimmt und aus diesem Wald

praktisch die Zweige unter einem aktuellen Knoten macht, was dann wieder einen Baum ergibt.

Dann ein Konstruktor Nill für den leeren Wald.

Und schließlich ein binärer Konstruktor Konz, der einen gegebenen Wald um einen Baum noch vergrößert.

So wir haben letztes Mal gesehen, vorletztes Mal, als wir über Mehrsortigkeit gesprochen haben,

dass diese Mehrsortigkeit sich überträgt auf die Algebren. Also die Algebren sind wieder

mehrsortig, genauso wie hier unsere Datentyp-Deklaration. Haben also Trägermengen für jede

der Sorten, die ich hier deklariere. Gut, gibt es einmal den Parameter Implizit, dieses a,

das fest interpretiert wird und dann gibt es eine Interpretation für jeden der Datentypen,

die ich hier deklariere. In diesem Falle also zwei, tree a und forest a. Und auch die

Homomorphismen zwischen diesen Algebren sind dann zweisortig, weil sie eben immer Bäume in

der einen Algebra auf Bäume in der anderen Algebra und forests in der einen Algebra auf forests in

der anderen Algebra abbilden müssen. Und aus, ja, es gibt natürlich ein forest nicht ein tree.

So und weil wir das Prinzip der primitiven Rekursion ja aus der Initialität unserer

Thermalgebra gewinnen, also über die Existenz bestimmter Homomorphismen, die also zweisortig

sind, ist auch dieses Prinzip der primitiven Rekursion eins zur Definition von in diesem

Falle zwei Abbildungen gleichzeitig. Das heißt, wenn ich eine rekursive Abbildung auf Bäumen

definieren will, muss ich gleichzeitig eine Abbildung auf Wäldern definieren. Und die

können sich dann gegenseitig verwenden, entsprechend den Patterns, die ich hier in

meinen Konstruktoren habe. Wir machen mal ein Beispiel.

So, nicht? Also nochmal hier das Schlagwort. Bei primitiver Rekursion habe ich immer eine Funktion

pro Sorte. Ja, man muss ein bisschen aufpassen. Ich habe hier nicht Parameter in Klammern

geschrieben. Natürlich gibt es, wenn ich mir die Definition von Homomorphismus angucke,

auch für die Parametersorten eine Abbildung. Nur diese Abbildung liegt fest, die ist immer

Identität. So, nicht? Also hier. Hier müssen wir also zwei Funktionen definieren, eine

auf Trees, eine auf Forests. So, machen wir das mal. Wir können zum Beispiel auf die Idee

kommen, einen Baum zu spiegeln. Spiegeln heißt, wir nehmen uns also an jeder Stelle die Liste

der Kinder und drehen die um. Gut, wie funktioniert das? Na, weil das immer zwei Funktionen sind,

fange ich an, die mit so einem zusätzlichen Buchstaben dahinter zu versehen, um die beiden

Funktionen zu unterscheiden. Jetzt kommt also erstmal diese Spiegelfunktion für Bäume,

MirrorT. So, auf Bäumen habe ich zwei Konstruktoren. Leaf und Node. So, ich muss also für jeden

dieser beiden Konstruktoren, muss ich angeben, eine Rekursive Klausel. Also, sagen wir mal,

das ist einfach ein Blatt, LeafX. Sehr gut, ein Baum, der nur aus einem Blatt besteht

zu spiegeln, das ist jetzt nicht so schwer, passiert nicht viel, weil da kommt also einfach

LeafX wieder raus. So, und dann kommt der Fall, dass wir einen Knoten in der Hand haben,

unter dem jetzt ein Wald kommt. So, und das Schema bleibt dasselbe wie bei der normalen

Rekursion. Ich darf jetzt hier rechts einen Rekursiven Aufruf machen auf die Konstruktorargumente,

in diesem Fall also auf das f. Aber da muss ich dann natürlich die passende Funktion

nehmen, f ist ja ein Wald. Das heißt, da muss ich die Funktion, die ich gleichzeitig

definiere, auf Wäldern nehmen. Also, gut, nicht was passiert, wenn ich spiegele. Nun,

das ist sicher immer noch ein Node, wird ja nicht plötzlich ein Blatt, nur davon, dass

ich spiegele. Und darunter kommen jetzt dieselben Äste nur umgedreht. Das heißt, jetzt kommt